The true abstract root of the Avail type lattice. It is pronounced top and written as the down tack (⊤) character. Every Avail value is an instance of ⊤, and every Avail type is a subtype of ⊤.

⊤ is distinct from any in that it includes exactly one additional value: the special value nil. This value does not satisfy any public protocol and is not available to an Avail programmer. It is, however, implicitly returned from every procedure, i.e., function whose return type is ⊤. Thus nil is the value produced iff no value is produced. The virtual machine uses nil to simplify several core algorithms, but exposure of nil to an Avail programmer would not yield a net good.

⊤ typically appears in Avail code in only a few select contexts:

• As the return type of a function type. In this context, it signifies that the function does not produce a value, i.e., it produces the unexposed value nil .
• As the return type of a continuation type. In this context, it signifies that the continuation will not produce a value, i.e., it produces the unexposed value nil .
• As the read type of a variable type. In this context, it signifies that no value may be read from the variable, i.e., the variable is write-only.
• As the idempotent initial value of an accumulator variable whose intermediate and final results represent a chain of type intersections. (Note that the type intersection of ⊤ with some type X is always X .)
• As the result of a semantic restriction on a procedure that serves only to reject parses based on the static types of the arguments (but does not strengthen the return type).
• As the result type of a phrase. In this context, it signifies that the phrase serves as a statement (and not merely as an expression).

A function whose declared return type is ⊤ is still permitted to answer an actual (non-{@code nil }) value. This is consistent with the type lattice, since every value is an instance of ⊤. It is useful, moreover, because a semantic restriction may strengthen the return type of a ⊤ -valued function at a particular call site to a subtype of ⊤.

⊤ is expressly forbidden from occurring in most contexts, including the following:

• As a parameter type of a function type.
• As the write type of a variable type. This also implies that it cannot be the type of an actual variable.
• As a leading type or the default type of a tuple type.
• As the element type of a set type.
• As the key type or value type of a map type.
• As the field type of an object type.
• As the type parameter of a pojo type.

Note that these prohibitions, when considered in aggregate, negate any possible value that could be gleaned from exposing the special value nil to an Avail program. They conspire together to ensure that nil could never be retained by an Avail value. It may therefore only exist as a temporary within a continuation, i.e., an item on the local stack of a function call. A reflective query of a continuation's temporaries that would answer nil will instead produce a variable whose read type is ⊥.